(include-book "generators/grid-data-generator")
(include-book "../src/acl2/image-handler")

;;This function will adjust the cells over in
;;the manner that is expected of the bitmap data
;;where the lowest y and x are actually set to zero
;;doing will be able to effectively prove that the
;;image the bitmap produces is the offset of the grid.
(defun adjust-cells (cells btm lft adjcells)
  (if (consp cells)
      (let* ((cur (car cells))
             (rest (cdr cells))
             (adjUp (+ (- 0 btm) (cell-y cur)))
             (adjLf (+ (- 0 lft) (cell-x  cur))))
        (adjust-cells rest 
                      btm
                      lft
                      (cons (cell adjLf adjUp) adjCells)))
      adjCells))
         

;; A check to make sure that any number generated
;; by the rowsize calculation is actually divisible
;; by 4 and it is the closest number possible.
(defproperty rowsize-calculation-test
  (width :value (random-integer))
  (let* ((rowsize (calculate-rowsize* width)))
    (equal (and (= (mod rowsize 4) 0)
                (< (- rowsize width) 4))
           t)))
         

;;A round trip test that given a random
;;life like grid generates a bitmap image and then
;;converts it back to get the same grid back.
;;The test must account for the information lost in
;;the bitmap conversion. Though the grid may have
;;negative values, the bitmap cannot.
;;To handle this
(defproperty lifelike-grid-to-bitmap-to-grid-test
  (size-x :value (random-between 1 100)
   size-y :value (random-between 1 100)
   density :value (/ (random-between 1 100) 100)
   grid :value (random-lifelike-grid size-x size-y density))
  (let* ((bitmap (image-generator* grid t))
         (bnds (get-ll-bounds grid))
         (btm (ll-bounds-bottom bnds))
         (lft (ll-bounds-left bnds)))
    (equal (nested-avl-flatten-to-cells 
            (read-image-to-grid* bitmap)) 
           (adjust-cells (reverse 
                          (nested-avl-flatten-to-cells grid))
                        btm
                        lft
                        nil))))

;;A round trip test that given a random
;;elementary grid generates a bitmap image
;;and then converts it back to the original grid.
(defproperty elementary-grid-to-bitmap-to-grid-test
  (size :value (random-between 1 100)
   density :value (/ (random-between 1 100) 100)
   grid :value (random-elementary-grid size density))
  (let* ((bitmap (image-generator* grid nil))
         (bnds (get-el-bounds grid))
         (lft (el-bounds-left bnds)))
    (equal (nested-avl-flatten-to-cells 
            (read-image-to-grid* bitmap)) 
           (adjust-cells (reverse 
                          (nested-avl-flatten-to-cells grid))
                        0
                        lft
                        nil))))



